COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	AN IDENTITY INVOLVING FUNCTIONS WITH PARAMETERS
C00006 ENDMK
C⊗;
AN IDENTITY INVOLVING FUNCTIONS WITH PARAMETERS


Consider a domain D and a continuous function F such that

(1)	F ε Dx(D→D)xD → D.

The example we have in mind is given by

	F(y,f,x) = if n x then y else a x . f(d x),

but it is not essential that  F  be this particular function, which
is related to  append by

	append(x,y) = F(y,λx.append(x,y),x).

We are going to form a function  g  in two ways.  First, we abstract
on  f  and  x  so as to get

	F(y) = λf.λx.F(y,f,x)

which is in ((D→D)→(D→D)) so that we can apply the  Y  combinator
and form

	g(y) = Y(λf.λx.F(y,f,x)),

an element of (D→D), and finally

	g = λy.Y(λf.λx.F(y,f,x)),

an element of (D→(D→D)).

Another way of getting  g  is to substitute for  f  in (1) a
an expression  f'(y)  where  f'(y) ε (D→D) and hence
f' ε (D→(D→D)), then abstract on f', y and x, getting

	F' = λf'.λy.λx.F(y,f'(y),x)

where  F' ε ((D→(D→D))→(D→(D→D)), which allows a further abstraction
giving

	g' = Y(F') = Y(λf'.λy.λx.F(y,f'(y),x)),

with  g' ε (D→(D→D)).

We assert that  g = g'.  Namely

	g(y,x)	= (λy.Y(λf.λx.F(y,f,x)))(y)(x)

		= Y(λf.λx.F(y,f,x))(x)

		= (λf.λx.F(y,f,x))(Y(λf.λx.F(y,f,x)))(x)

		= F(y,Y(λf.λx.F(y,f,x)),x)

		= F(y,g(y),x),

whereas

	g'(y,x)	= Y(λf'.λy.λx.F(y,f'(y),x))(y)(x)

		= λf'.λy.λx.F(y,f'(y),x)(Y(λf'.λy.λx.F(y,f'(y),x)))(y)(x)

		= F(y,Y(λf'.λy.λx.F(y,f'(y),x))(y),x)

		= F(y,g'(y),x).

Thus  g  and  g'  satisfy each others functional equations, and so
by recursion induction and a little hand waving are equal.  Equating
out the right hand sides, we have

	λy.Y(λf.λx.F(y,f,x)) = Y(λf'.λy.λx.F(y,f'(y),x))

and transforming both sides of the equation, we get

	λy.Y(F(y)) = Y(λf'.λy.F(y)(f'(y))

and

	B(Y,F) = Y(λf'.λy.S(F,f',y))

		= Y(S(F))

		= B(Y,S)(F),

and abstracting on  F  which is arbitrary, we get finally

	B(Y) = B(Y,S).

This identity, which I suppose must be well known is simpler in
its combinatory form than in its λ-calculus form.